\begin{tabbing}
$\forall$$i$, $a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]@$i$ \=(with ds: ${\it ds}$\+
\\[0ex]action $a$:$T$
\\[0ex]precondition $a$(v) is
\\[0ex]$P$ s v) 
\-\\[0ex]realizes ${\it es}$.
\\[0ex]@$i$ \=Precondition for $a$(v)\+
\\[0ex]$P$ State(${\it ds}$) (v:$T$)
\-
\end{tabbing}